COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.device XGP
C00004 00003	.onecol BEGIN "TITLE PAGE"
C00005 00004	.BEGIN "COVER PAGE"
C00008 00005	.EVERY HEADING(%3{SECNAME},{SSNAME},{PAGE!}) page←0 twocol cb Abstract
C00044 00006	.cb Personnel
C00051 00007	.onecol cb Budget
C00056 00008	.twocol bib
C00061 00009	.skip 200
C00063 ENDMK
C⊗;
.device XGP;
.require "bask.pub[sub,sys]" source_file;
.font 5 "gacs25";
.font 6 "clar30"
.font 9 "sail25"
.sides←1;
.require "twocol.pub[sub,sys]" source_file;

.MACRO YON(LBL)  ⊂ "Section "; SUB2! LBL ⊃;

.MACRO BC ⊂ BEGIN PREFACE 0; INDENT 1,4; CRBREAK nojust ⊃

.MACRO BS ⊂ BEGIN PREFACE 0; INDENT 1,4; nojust ⊃

.MACRO SUB(IND) ⊂ INDENT 0,IND; TABS IND+1;⊃

.MACRO IB ⊂ turn on "%";
.AT """" ⊂ (IF THISFONT=1 THEN "%3" ELSE "%1"); ⊃
.AT "<" ⊂ "%2" ⊃;  AT ">" ⊂ "%1" ⊃;
. ⊃

.MACRO BIB  ⊂  CB(References);
.	BEGIN INDENT 0,3; NOJUST; IB;
.	AT "AIM-" ⊂ "Stanford AI Memo AαIαMα-" ⊃;
.	COUNT exref TO 200
.	AT "⊗" ⊂ IF LINES<3 THEN NEXT COLUMN; NEXT EXREF; ("["&EXREF&"]  ") ⊃
.	⊃
.
.COUNT ITEM
.AT "#" ⊂NEXT ITEM;(ITEM!);⊃;

.SECNAME←"";
.portion some; place text;
.every heading();
.onecol; BEGIN "TITLE PAGE"
.SKIP TO COLUMN 1;
.CENTER;
.PREFACE 0;
.SELECT 1;
Research Proposal Submitted to
.SKIP 2;
%3THE NATIONAL SCIENCE FOUNDATION
.SKIP 2;
%1for
.SKIP 2;
%3Basic Research in Artificial Intelligence
.SKIP 2;
%1by
.SKIP 2;
John McCarthy
Professor of Computer Science
Principal Investigator
.SKIP 8;
July 1977
.SKIP 5;
Computer Science Department
.SKIP 1;
%3STANFORD UNIVERSITY
.SKIP 1;
%1Stanford, California
.END "TITLE PAGE";
.BEGIN "COVER PAGE"
.SKIP TO COLUMN 1;
.NOFILL;
.PREFACE 0;
.INDENT 0,0,0;
.SELECT 1;
.TURN ON "\↓_";
.AT "≤≤" TXT "≥" ⊂ }↓_%9TXT%*_↓{ ⊃;
.	BEGIN "COVER PAGE TITLE"
.	CENTER;
.	SELECT 6;
Research Proposal Submitted to the National Science Foundation
.	END "COVER PAGE TITLE";
.SKIP 5;
.SELECT 1;
Proposed Amount ≤≤$xx,xxx≥ Proposed Effective Date ≤≤1 Jan. 1978≥ Proposed Duration ≤≤3 years≥
.SKIP 3;
Title ≤≤Basic Research in Artificial Intelligence≥
.TABS 40;
.SKIP 3;
Principal Investigator ≤≤John McCarthy≥\Submitting Institution ≤≤Stanford University≥
  Soc. Sec. No. ≤≤558-30-4793≥\Department ≤≤ Computer Science    ≥
\Address ≤≤Stanford, California 94305≥
.SKIP 3;
Make grant to ≤≤Board of Trustees of the Leland Stanford Junior University≥
.SKIP 3;
Endorsements:
.TABS 10,35,59;
.SKIP 1;
\Principal Investigator\Department Head\Institutional Admin. Official
.TABS 10,35,60;
.PREFACE 1;
Name\≤≤John McCarthy        ≥\≤≤Edward A. Feigenbaum ≥\≤≤                     ≥
.SKIP 1;
Signature\≤≤                     ≥\≤≤                     ≥\≤≤                     ≥
Title\≤≤Professor            ≥\≤≤Professor & Chairman ≥\≤≤                     ≥
Telephone\≤≤(415) 497-4430       ≥\≤≤(415) 497-4079       ≥\≤≤                     ≥
Date\≤≤                     ≥\≤≤                     ≥\≤≤                     ≥
.END "COVER PAGE";
.EVERY HEADING(%3{SECNAME},{SSNAME},{PAGE!}); page←0; twocol; cb Abstract
.fill adjust
	This is a request for a grant
in support of basic research in artificial intelligence
with emphasis on the structure of formal reasoning and
computer proof checking.  The computer proof checking supports the
basic research in AI, but also has applications to verifying
computer programs and is independently valuable.

.cb Introduction

	Artificial intelligence has proved to be a difficult branch
of science.  Some people thought that human level intelligence
could be achieved in ten or twenty years, but this was based on
the difficulties they could see when they made the optimistic
predictions.  Our own opinion is that major scientific discoveries
remain to be made.
Moreover, many of these discoveries require theoretical advances and
not merely the extension of current ideas for producing "expert programs"
to new domains.
The increasing emphasis by ARPA and other agencies sponsoring AI
research on immediate applications has resulted in a serious
imbalance.  Deciding what the basic issues are is difficult
enough without having formulate everything in terms of demonstration
programs to be available in two years.

	Our research is based on the idea that for many purposes,
the problems of artificial intelligence can be separated into two
parts - an epistemological part and a heuristic part.
The %2epistemological%1 part concerns what facts and inference
rules are available for solving a problem and how they can be
represented in the memory of a computer, and the heuristic part
concerns procedures for deciding what to do on the basis of the
necessary facts.  Most work in AI has concerned the %2heuristics%1,
and computer representations of information have been chosen that
are capable of representing only a part of the information that
would be available to a human.  The modes of reasoning used by
present programs are often even weaker than the representations
themselves.

	The lines of research we plan to pursue are exemplified in
the attached reprints and preprints.  Here we shall explain how this
work fits together.  Our long range goal is a program that can be told
facts about the world and can use them effectively to achieve the
goals it is given.
Sometimes it will use the facts directly from its data base using
deductive and inductive processes like the deductive processes
of mathematical logic.  However, we are already sure, (McCarthy 1977a),
that conjectural processes will be needed that go beyond deduction
as presently conceived.  Sometimes it will use these facts to compile
"expert programs" that use these facts in a more efficient way than
simple reasoning.  However, the expert programs will have to defer
to reasoning when unexpected use of the factual data-base is required.

	We do not propose to implement such a program immediately -
maybe not at all within the next five years.  This is because its
success depends on successful formalization of facts about the world.
We have made progress in this formalization, but we may be occupied
with it exclusively for the forseeable future.  In short we will
emphasize theoretical artificial intelligence except for the work
with proof-checkers to be described below.

	The main areas of our previous accomplishment and future work
are the following (as now seen):

.item← 0

#. Development of %2circumscription%1 as a mode of reasoning and its
application to artificial intelligence.  %2Circumscription%1 formalizes
the process of concluding (often incorrectly) that a certain collection
of facts is all that are relevant for solving a problem.  It does this
by allowing one to formally assume that the entitities that are generated
by specified processes are all the entities of a specified kind.
This is common in human reasoning and, for reasons described in the preprint,
cannot be accomplished by any form of deduction.

#. Development of treating concepts as objects.  This, described in
(McCarthy 1977b) facilitates, and may be required for, reasoning about
knowledge, belief, wants, possibility and necessity.

#. The current biggest gap in computer reasoning about the physical world
is the complete lack of a system for reasoning about concurrent processes.
All the current problem solving programs assume that each action of the
program produces a next state that depends on the current state, the action,
and sometimes on a random variable.  They don't take into account continuous
processes or the fact that other actions and events may be taking place.
We believe that circumscription may be important in formalizing what
people know about such processes.

#. We also plan some study of the theory of patterns, especially higher
order patterns in which function variables may be matched and relations
between patterns - for example, the relation between a pattern describing
a type of three-dimensional object such as a person or a vehicle and its
patterns of its perception - such as its projection on a retina as modified
by angle of vision, lighting and occlusion by other objects.

	In all this work, the emphasis is on representation of the information
that is actually available to an observer with given opportunities to
observe and compute.


.cb Proof Checking by Computer

	We must distinguish theorem proving by computer from proof-checking
by computer.

	It is an essential part of the notion of proof in a formal
system that a candidate proof can be checked by a mechanical process.
It is a consequence of the work of Goedel, Church and Turing that
no mechanical process can always determine whether a proof of a
given sentence exists in a formal system.
In principle, therefore, proof-checking should be easy, while all
the difficulties of understanding the creative processes of a
mathematician are involved in making a high powered theorem prover.

	However, in spite of the simplicity of modern logical and set
theoretic systems and the brevity with which they permit axiomatizing
mathematical and physical systems, checking actual proofs
has encountered formidable difficulties.  It is easy enough to make
proof-checkers for the formal systems in logic and set theory textbooks,
and we did it some years ago.  The difficulty is that the formal proofs of easy
theorems turn out to be ten times longer than informal proofs, and the
excess in length grows the further one advances into the theory.  The
trouble is that mathematicians have not succeeded in completely formalizing
the languages and reasoning processes they actually use.  Much reasoning
that at first seems to be within a given mathematical system, actually is
metamathematical reasoning about the system.  Even when a mathematician
is working within a system, he establishes shortcuts whose repeated use
keeps down the length of a proof.

	We have a proof-checker called FOL (for first order logic) (Weyhrauch
1977a), we have been improving it since 1973, and we propose to improve
it further under this grant.  (Rewriting it from scratch will be required
at some point, but we aren't sure when this will be the best use of
limited manpower).  With FOL, we have checked a variety of mathematical
proofs, and each such project has told us something about how to improve
the proof-checker or how to formalize a given mathematical domain or
how to write and debug proofs.  The proofs described below
each tested the adequacy of FOL and our axiomatizations.

(a) Any device capable of accepting general mathematical reasoning must be 
able to prove theorems of arithmetic.  We chose "if p is a prime number and 
p divides the product a*b, then p divides a or p divides b." as a typical
example.

(b) The adequacy of FOL's set theory was tested by checking both Lagrange's 
theorem and Ramsey's theorem.  These are well known theorems of mathematics.
[Lagrange's theorem: the order of a subgroup of a group G divides the order 
of G; Ramsey's theorem: let G be a countably infinite set of points, each 
point being connected to every other by a thread, each thread being red or
black.  Then there is an infinite subset of these points such that the 
connecting threads within the subset are all of the same color.]

(c) Wilson's theorem that "If %2p%1 is prime, then %2p%1 divides %2(p-1)!%1"
is a purely arithmetic statement, but its proof uses a 
pairing argument (requiring set theory) which is beyond the capability of 
present theorem-proving programs.  

(d) We checked the first one hundred theorems of set theory as presented 
in (Kelley 1955).  This established a large collection
of proofs to be used as benchmarks to measure later ideas.  

(e) The problem of formalizing how we can reason about what other people
know was studied by axiomatizing the wise man problem (McCarthy %2et. al%1
1977e) and (Sato 1977).  One of the hard problems here was to formulate
and prove that some else doesn't know something.  This problem was also
axiomatized in second way by Chris Goad (Goad, in progress).

(f) We proved the correctness of the McCarthy-Painter compiler (McCarthy
and Painter 1967).  This allowed us to compare the original first order
proof with some more recent proofs (Weyhrauch and Milner 1972; Boyer and
Moore 1975).

	Recent improvements have reduced the length of some proofs by
a factor of better than ten.  Here are some of them and what they have
accomplished.

	After a period of adding new features to FOL we have again begun to 
experiment with proofs and our initial successes are encouraging.  These
recent improvements have reduced the length of some
proofs by a factor of better than ten.  The reducing the lengths of proofs
does not by itself mean that we are getting anywhere.
Some of the proofs we are now producing are about as long as
their informal versions.  This is most clearly evident in
the %2samefringe%1 example below.  Here are three of our recent
experiments:

	Filman (Filman, in progress) has used FOL to show that the
reasoning involved in the solution of a hard retrospective chess problem
can be formalized in first order logic.  We chose this example from
outside mathematics, because human reasoning often mixes deduction with
observation of the outside world, and observation of a chess %2partial
position%1 is prominent in this example.  The semantic attachment
mechanism of FOL was used to build a simulation of his chess world.  He
could then use the semantic simplification routines of FOL to answer (in a
single step) questions like "is he black king in check on board B" by
looking at his model, rather than deducing from axioms about the rules of
chess that black was in check.  This single use of semantic attachment
saves several hundered steps over traditional formalizations.  Filman's
proof is still much longer than the informal proof, showing that we still
don't fully understand how humans combine observation with deduction.

	We have preliminary estimates of the length of the
Kelley set theory proofs mentioned above.  In an initial experiment
using only part of the currently available features, we reduced the number
of steps necessary to prove the first thirty three theorems from 461 to 104.
Considering that it takes one step just to express the theorem, this is
quite impressive.  We expect that adding the goal-structure features mentioned
below will substantially reduce these proof lengths.

	In connection with McCarthy's recent (McCarthy 1977d)
formalization of LISP programs using sentences and schemata of first order
logic, we have checked a FOL proof of the correctness of his
%2samefringe%1 program.  %2samefringe[x,y]%1 is turns true if the
S-expressions %2x%1 and %2y%1 have the same atoms in the same order.  This proof
as checked by FOL was of the same length as a written out informal proof
of the same result.  We believe that such favorable results are generally
possible.

	Our plans for FOL include the following:

(1) The verification of the correctness of LISP programs.  John
McCarthy (McCarthy 1977d)
has recently begun using axiom schemas to prove the
properties of LISP programs.  We intend to expand this work by introducing
meta-mathematical machinery into FOL (see below).  This will be followed
by a major effort to use McCarthy's axiomatization of LISP and to prove
properties of simple LISP programs.  Weyhrauch has recently pointed out
that this same technique can be used to formulate part of Dana Scott's
computation induction into first order logic.  This also requires the
metamathematical machinery.  We expect this to be sufficiently practical
for us to use this axiomatization in Stanford LISP courses.

(2) Another aspect of program verification are what are called intensional
properties of programs.  These include things like how much storage a
program uses, and how many steps it takes.  These questions cannot be
asked by current formalisms for mathematical theory of computation.  The
require theories that contain programs as objects and can talk about the
abstract properties of the machines that they run on.  Most previous
formal efforts have only shown properties of the algorithms computed by
programs, not properties of programs themselves.  One exception was the
work of Aiello, Aiello, and Weyhrauch (Aiello 1974) on PASCAL.  This was
carried out using another formal system and we have just begun to think
about such problems using first order logic.

(3) The verification of the correctness of hardware circuit design using
FOL continuing the work of Wagner (Wagner 1977).  Almost all present
hardware verification is based on simulating it in all posible states.
Wagner demonstrated that formal proofs that the hardware is correct are
feasible and require less human and computer work than the simulation
techniques.  We propose to continue this work.

(4) We intend to redo the theorems of Kelley mentioned above using
the many new features that have been added to FOL.  These include
the syntactic simplifier, the semantic attachment mechanism, and various
decision proceedures.

(5) Introducing metamathematical machinery into FOL will allow us
stating and proving theorems about how we do reasoning in the 
logic.  The implications of this are very broad.  As mentioned above we 
will be able to state, as sentences of the metamathematics, axiom schemas
useful in proving the correctness of LISP programs.  Another application
of schemas is to axiomatizing circumscription.

(6) The usefulness of the metamathematics will be enhanced by our addition
of certain reflection principles.  These are rules that state some relation
between a theory and its metamathematics.  For example, if
you have proved a certain formula, then in the meta-theory you can assert
that the formula is provable.  Conversely, informal mathematics often uses
metamathematical assertions that all formulas with certain properties are
true.  The attachment mechanism combined with reflection principles
will allow us to automatically use such metatheorems
to prove theorems in the base theory.
.cb Personnel

Richard Weyhrauch is the main designer and implementer of FOL.  This requires
a full understanding of both modern mathematical logic, programming
techniques and the ability to do good human engineering.

The FOL project attracts considerable interest from young mathematicians
who would like, finally, to see computers applied to mathematical research
in a significant way.  A rotating research associateship will benefit both
proof-checking research
and the propagation of its results.

.cb Biography of John McCarthy

.begin nojust; indent 0,4;
BORN:  September 4, 1927 in Boston, Massachusetts

EDUCATION:
.preface 0; crbreak;
B.S.  (Mathematics) California Institute of Technology, 1948.
Ph.D. (Mathematics) Princeton University, 1951.
.skip
HONORS AND SOCIETIES:
American Mathematical Society,
Association for Computing Machinery,
Sigma Xi,
Sloan Fellow in Physical Science (1957-59),
ACM National Lecturer (1961),
IEEE,
A.M. Turing Award from Association for Computing Machinery (1971).
.skip
PROFESSIONAL EXPERIENCE:
Proctor Fellow, Princeton University (1950-51),
Higgins Research Instructor in Mathematics, Princeton University (1951-53),
Acting Assistant Professor of Mathematics, Stanford University (1953-55),
Assistant Professor of Mathematics, Dartmouth College (1955-58),
Assistant Professor of Communication Science, M.I.T. (1958-61),
Associate Professor of Communication Science, M.I.T. (1961-62),
Professor of Computer Science Stanford University (1962 - present).
.skip
PROFESSIONAL RESPONSIBILITIES AND SCIENTIFIC INTERESTS:
.crspace;
With Marvin Minsky organized and directed the Artificial Intelligence
Project at M.I.T.

Organized and directs Stanford Artificial Intelligence Project.

Developed the LISP programming system for computing with
symbolic expressions, participated in the development
of the ALGOL 58 and the ALGOL 60 languages.

Present scientific work is in the fields of Artificial
Intelligence, Computation with Symbolic Expressions,
Mathematical Theory of Computation, Time-Sharing computer
systems. 

PUBLICATIONS:
.count ref inline; at "⊗" ⊂next ref; ("["&ref&"]  ");⊃
.  at "<" ⊂"%2"⊃; at ">" ⊂"%1"⊃;

⊗"Towards a Mathematical Theory of Computation", in
<Proc. IFIP Congress 62>, North-Holland, Amsterdam, 1963.

⊗"A Basis for a Mathematical Theory of Computation",
in P. Braffort and D. Hershberg (eds.), <Computer Programming and
Formal Systems>, North-Holland, Amsterdam, 1963.

⊗(with S. Boilen, E. Fredkin, J.C.R. Licklider)
"A Time-Sharing Debugging System for a Small Computer", <Proc.
AFIPS Conf.> (SJCC), Vol. 23, 1963.

⊗(with F. Corbato, M. Daggett) "The Linking
Segment Subprogram Language and Linking Loader Programming
Languages", <Comm. ACM>, July 1963.

⊗"Problems in the Theory of Computation", <Proc. IFIP
Congress 1965>.

⊗"Time-Sharing Computer Systems", in W. Orr (ed.),
<Conversational Computers>, Wiley, 1966.

⊗"A Formal Description of a Subset of Algol", in T.
Steele (ed.), <Formal Language Description Languages for Computer
Programming>, North-Holland, Amsterdam, 1966.

⊗"Information", <Scientific American>, September
1966.

⊗"Computer Control of a Hand and Eye", in <Proc.
Third All-Union Conference on Automatic Control (Technical
Cybernetics)>, Nauka, Moscow, 1967 (Russian).

⊗(with D. Brian, G. Feldman, and J. Allen) "THOR -- A
Display Based Time-Sharing System", <Proc. AFIPS Conf.> (FJCC), Vol.
30, Thompson, Washington, D.C., 1967.

⊗(with James Painter) "Correctness of a Compiler for
Arithmetic Expressions", Amer. Math. Soc., <Proc. Symposia in
Applied Math., Math. Aspects of Computer Science>, New York, 1967.

⊗"Programs with Common Sense", in Marvin Minsky
(ed.), <Semantic Information Processing>, MIT Press, Cambridge, 1968.

⊗(with Lester Earnest, D. Raj. Reddy, Pierre Vicens) "A
Computer with Hands, Eyes, and Ears", <Proc. AFIPS Conf.> (FJCC),
1968.

⊗(with Patrick Hayes) "Some Philosophical Problems from the
Standpoint of Artificial Intelligence", in Donald Michie (ed.),
<Machine Intelligence 4>, American Elsevier, New York, 1969.

⊗"The Home Information Terminal", <Man and Computer,
Proc. Int. Conf., Bordeaux, 1970>, S. Karger, New York, 1972.

.end
.onecol; cb Budget
.begin "budget" verbatim select 5;

PERIOD COVERED: 3 Years: 1 Jan. 1978 through 31 December 1980.

Dates:                1/1/78-12/31/78   1/1/79-12/31/79   1/1/80-12/31/80

A. SALARIES AND WAGES

   1.Senior Personnel:

     a.John McCarthy,      7,575.            8,181.           8,835.
       Professor
       Summer 75%
       Acad. Yr. 0%

   2.Other Personnel

     a.Research Associates

       (1)R.Weyhrauch     10,400.           11,232.          12,131.
          50% - 12 months
                                
       (2) ________,      17,000.           18,360.          19,829.
          100% - 12 months

     b. Student Research 
        Assistants
        (50% Acad.Yr.;
        100% Summer)

       (1)	           7,155.            7,704.           8,320.

       (2)                 7,155.            7,704.           8,320.

     c. Support Personnel

       (1)Secty(25%)       2,615.            2,824.           3,050.
    
       (2)Elec.Tech.(25%)  4,895.            5,287.           5,710.
                          _______           _______          _______

   Total Salaries & Wages 56,795.           61,292.          66,195.

B. STAFF BENEFITS         
   9/1/77-8/31/78:20.0%          
   9/1/78-8/31/79:20.8%
   9/1/79-8/31/80;21.6%                                          
   9/1/80-8/31/81;22.4%
                          11,510.           12,912.          14,475.
                          _______          ________         ________
C. TOTAL SALARIES, WAGES,
   AND STAFF BENEFITS     68,305.           74,204.          80,670.

.next page
D. PERMANENT EQUIPMENT        --                --               --

E. EXPENDABLE SUPPLIES     2,040.            2,040.           2,040.
   & EQUIPMENT(e.g.,copying,
   office supplies, postage,      
   freight, consulting,
   honoraria)

F. TRAVEL                  2,300.            2,300.           2,300.
   All Domestic Travel

G. PUBLICATIONS	           1,200.            1,200.           1,200.

H. OTHER COSTS             8,300.            8,300.           8,300.
   1.Communication  2,000.
     (telephone)     
   2. Computer      6,300.
      Equip. Maint.
                          _______          ________          _______  

I. TOTAL COSTS             82,145.          88,044.          94,510.
    (A through H)

J. INDIRECT COSTS:58% of   47,644.          51,066.          54,816.
   A through H, less D.   ________         ________         ________     


K. TOTAL COSTS            129,789.         139,110.         149,326.
.end "budget"
.twocol; bib;

%3Aiello, L., Aiello, M., and Weyhrauch, R.%1 (1974) The Semantics of PASCAL in LCF,
Stanford: AIM-221.  Available as α<Arpanet:SAILα> αAIM221.PUB[DOC,RWW].

%3Boyer, R.S., and Moore, J.S.%1 (1975) Proving Theorems About LISP Functions,
JACM Vol 22. No. 1 pp. 129-144. New York: ACM.

%3Filman, R.E.%1 (in progress) Explorations in Representations: The Chess Domain.

%3Goad, Christopher%1 (in progress) A Model Theoretic Solution of the 
Wise Man Problem.

%3Kelley, J.L.%1 (1955) General Topology, Princeton, New Jersey: D. Van
Nostrand Company, Inc.

%3McCarthy, J. and Painter, J.%1 (1967) Correctness of a Compiler for
Arithmetic Expressions.  %2Proc. Symposia in Applied Math., Math. Aspects
of Computer Science%1 New York: Amer. Math. Soc..

%3McCarthy, J. and Hayes, P.J.%1 (1969) Some Philosophical Problems from
the Standpoint of Artificial Intelligence. %2Machine Intelligence 4%1,
pp. 463-502 (eds Meltzer, B. and Michie, D.). Edinburgh: Edinburgh
University Press.

%3McCarthy, J.%1 (1977a) Minimal Inference - A New Way of Jumping
to Conclusions (to be published).  Available as α<Arpanet:SAILα> MINIMA.[S77,JMC].

%3McCarthy, J.%1 (1977b) First Order Theories of Individual Concepts
(to be published).  Available as α<Arpanet:SAILα> CONCEP.[E76,JMC].

%3McCarthy, J.%1 (1977c) Ascribing Mental Qualities to Machines (to
be published).  Available as α<Arpanet:SAILα> MENTAL.[F76,JMC].

%3McCarthy, J. %1 (1977d) First-Order Representation of Recursive Programs,
(to be published).  Available as α<Arpanet:SAILα> FIRST.NEW[W77,JMC].

%3McCarthy, J., Sato, M., Hayashi, T. and Igarashi, S.%1 (1977e)
On the Model Theory of Knowledge.  Presented at %2IJCAI-1977%1;
to appear in the %2SIGART Newsletter%1.

%3Moore, Robert C.%1 (1977) Reasoning about Knowledge and Action, %21977
IJCAI Proceedings%1.  Available as α<Arpanet:SAILα> IJCAI.PUB[1,RCM].

%3Sato, M.%1 (1977) A study of Kripke-type Models for some Model Logics
by Gentzen's Sequential Method, (to appear in Publ. R.I.M.S., Kyoto University).

%3Wagner, Todd J.%1 (1977) Hardware Verification.  Ph.D. thesis, Stanford
University.  Available as α<Arpanet:SAILα> THESIS.PUB[THE,TJW].

%3Weyhrauch, R. W., and Milner, R.%1 (1972) Program Semanantics and
Correctness in a Mechanized Logic.  %2First USA - Japan Computer Conference
Proceedings.%1 Tokyo: Hitachi Priniting Company.

%3Weyhrauch, R. W.%1 (1977a) A Users Manual for FOL. Stanford: AIM-235.1.
Available as α<Arpanet:SAILα> FOLMAN.PUB[DOC,RWW].

%3Weyhrauch, R. W. (ed.)%1 (1977b) A Collection of FOL Proofs (to be
published).
.end
.skip 200;
Notes for NSF proposal

What: Proof checking, epistemology, general basic research.

What has been done: LCF, FOL, McCs epistemology and MTC.

Who: Weyhrauch, JMC part time, research fellow as visitor, 4 graduate
students, disk file, terminals.

Publications:

	Recently Todd Wagner completed a thesis (Wagner 1977) on
hardware verification using FOL.  It turns out that almost all
hardware verification has used simulation, and simulation can
never be complete.  Wagner has shown that proving hardware correct
at the level of gates and flip-flops is well suited to proof-checking,
because the problems of mathematical induction that arise in program
verification usually don't arise.

	The application of first order logic to verifying programs
has been stimulated by the discovery (McCarthy 1977c) that recursive
programs can be nicely characterized by a first order functional
equation and a first order minimization schema.  Almost all reasonable
extensional properties of pure LISP programs should be conveniently 
provable.  We propose to investigate these questions further in the
next time period.